theory TEEC_SEC_Common
imports Main "../GPTEE_Instantiation"
begin

section "Auxiliary lemmas"

subsection "foldl related"
consts session_id1::SESSION_ID_TYPE
lemma foldl_once:"TEE_state s = TEE_state (updateListForTEECCS s session_id1)" using updateListForTEECCS_def 
by simp

lemma foldl_induct_rule:"⋀ s lst.  (TEE_state s = TEE_state (foldl updateListForTEECCS s lst))"
apply(rule rev_induct)
using updateListForTEECCS_def apply simp+
done

lemma foldl_induct_rule2:"⋀ s lst.  (ree_total_size(REE_state s) = ree_total_size(REE_state (foldl updateListForTEECCS s lst)))"
apply(rule rev_induct)
using updateListForTEECCS_def apply simp+
done

lemma foldl_induct_rule3:" (driver_mem(REE_state s) = driver_mem(REE_state (foldl updateListForTEECCS s lst)))"
proof(induct lst rule:rev_induct)
case Nil
then show ?case 
    by simp
next
case (snoc x xs)
then show ?case 
    using updateListForTEECCS_def
    by simp
qed
 

subsection "newID related"

(*
definition TA_OpenSessionEntryPoint2::"Sys_Config⇒State⇒TEEC_Operation⇒THREAD_ID_TYPE⇒State" where
          "TA_OpenSessionEntryPoint2 sc s opt tid≡ 
                                         SOME s1.
                                               REE_state s1 = REE_state s∧
                                              ( filter (λx. ownership x≠tid) (tee_memories(TEE_state s1) )  
                                                  =( filter (λx. ownership x≠tid) (tee_memories(TEE_state s))))  "
                                             
                                               
  
*)



(*
lemma newId_in:" (SOME newId. newId ∈ (UNIV  -{(0::nat)} -{(1::nat)})) ∈(UNIV -{(0::nat)} - {(1::nat)})" 
apply(simp add:someI)
apply auto
prefer 2
apply (metis (mono_tags, lifting) Suc_less_eq2 le_imp_less_Suc less_numeral_extra(4) some_eq_imp zero_le_one zero_less_one)
using some_eq_imp nat.distinct(1)
by (metis (mono_tags, lifting) n_not_Suc_n neq0_conv) 

definition newIdFromList1 :: "nat list ⇒ nat" where
  "newIdFromList1 idList ≡ SOME newId. newId∈({2..})"

definition newIdFromList2 :: "nat list ⇒ nat" where
  "newIdFromList2 idList ≡ SOME newId. newId∈({(2::nat)..}-(set idList))"


lemma newIdFromList1_not_zero:"∀lst.(0::nat)≠(newIdFromList1 lst)"
apply(simp add:newIdFromList1_def someI)
using  some_eq_imp 
by (metis le_refl neq0_conv not_numeral_le_zero)

lemma new_pre:"∀idList. ({2..}-(set idList))⊆({2..})" by simp

lemma all_pre1:"∀A B. A⊆B∧(∀x∈B. x≥(2::nat))⟶(∀y∈A. y≥(2::nat))" by blast 

lemma filter_related_aux:
    "∀lst lst'. ((filter (λx. (block_id x) = (0::nat)) lst) = (filter (λy. (block_id y) = (0::nat)) lst')
              ⟶ {x. x∈set(lst)∧ (block_id x=(0::nat))} =
                           {x. x∈set(lst')∧ (block_id x=(0::nat))})"
  apply auto
  using  member_filter
  apply (metis (mono_tags) filter_set) 
  by (metis (mono_tags) filter_set member_filter)


lemma filter_pre_aux:
    "∀lst lst' new.  (lst'=⦇block_id = new,size=x::nat,ownership = y::nat,
                                              access_right = z::nat list,is_Shared=h::bool⦈#lst ∧new≠0
              ⟶(filter (λx. (block_id x) = (0::nat)) lst) = (filter (λx. (block_id x) = (0::nat)) lst'))"
by auto



lemma q1:" newIdFromList lst∉set lst"
proof -
{
  have a1:"(SOME a. (a≥(2::nat))∧a∉set lst)∉set lst" using some_eq_imp newIDexist newIdFromList_def
    by (metis (mono_tags, lifting))
  show ?thesis using a1 newIdFromList_def by simp
}qed


lemma q2:"y∈(set lst)∧x=newIdFromList lst⟶x≠y"
proof -
{

assume a1:"x=newIdFromList lst"
assume a2:"y∈(set lst)"

have a3:"x∉set lst"  using q1 a1 by blast
have a4:"x≠y" using a3 a2 by blast

}
then show ?thesis by blast
qed

lemma q3:"∀x y lst. y∈(set lst)∧x=newIdFromList lst⟶x≠y"
 using q2 by simp

(*
lemma q4:"∀x y. x≠y∧x∈set(tee_memories(TEE_state s)) ∧ y∈set(tee_memories(TEE_state s)) ∧ block_id x ≠ block_id y" 
sorry
*)


*)


lemma max_aux:"∀x::nat ∈ set lst. foldr max lst a≥x"
apply(induct lst)
by auto

lemma newIDexist:" ∃a. (a≥(2::nat)∧a∉set lst)"
proof -
{
define a where "a=Suc (foldr max lst 1)"
have "∀x∈set lst. a>x" using max_aux 
by (simp add: ‹a = Suc (foldr max lst 1)› less_Suc_eq_le)
moreover have "a≥2"
apply(simp add:a_def)
apply(induct lst)
by auto
ultimately have "a≥2∧a∉set lst" by blast
then show ?thesis by blast

}qed


lemma newIdFromList_not_zero:"∀lst.(0::nat)≠(newIdFromList lst)"
apply(simp add:newIdFromList_def someI)
apply auto
proof -
{
fix lst::"nat list"
 have "(SOME a. (a≥(2::nat))∧a∉set lst)≠0" using some_eq_imp newIDexist
    by (metis (mono_tags, lifting) le0 le_antisym neq0_conv numeral_2_eq_2 zero_less_Suc)
}
then show "⋀lst. 0 < (SOME newId. (2::nat) ≤ newId ∧ newId ∉ set lst)" by blast
qed


lemma newBlockID_not_zero:"∀s. newMemBlockID s ≠0"
apply simp
apply(simp add:newMemBlockID_def)
 using  newIdFromList_not_zero by simp

lemma newBlockID2_not_zero:"∀s. snd(newMemBlockID2 s) ≠0"
apply simp
apply(simp add:newMemBlockID2_def)
 using  newIdFromList_not_zero
 by (metis snd_conv zero_less_Suc) 

lemma newBlockID3_not_zero:"∀s. newMemBlockID3 s ≠0"
  using system_init_def newMemBlockID3_def
    by simp

lemma filter_pre:
    "∀s s' new.  ((tee_memories (TEE_state s')))=⦇block_id = new,size=x::nat,ownership = y::nat,
                                              access_right = z::DOMAIN_ID ⇒ MEM_RIGHT option,is_SecureMem=h::bool,related = None⦈#(tee_memories (TEE_state s)) ∧new≠0
              ⟶(filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s')))"
by auto

lemma filter_pre2:
    "∀s s' new.  ((tee_memories (TEE_state s')))=⦇block_id = new,size=x::nat,ownership = y::nat,
                                              access_right = z::DOMAIN_ID ⇒ MEM_RIGHT option,is_SecureMem=h::bool,related = None⦈#(tee_memories (TEE_state s)) ∧new≠0
                  ∧ (BIDpointer(ta_mgr(TEE_state s')) = BIDpointer(ta_mgr(TEE_state s)) +1)
              ⟶(filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s')))"
by auto


lemma filter_related:
    "∀s s'. ((filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories (TEE_state s')))
              ⟶ {x. x∈set((tee_memories (TEE_state s)))∧ (block_id x=(0::nat))} =
                           {x. x∈set((tee_memories (TEE_state s')))∧ (block_id x=(0::nat))})"
  apply auto
  using  member_filter 
  apply (metis (mono_tags) filter_set) 
  by (metis (mono_tags) filter_set member_filter)

lemma filter_related_TA:
    "∀s s' tid. ((filter (λx. (ownership x≠tid)) (tee_memories (TEE_state s))) = (filter (λx. (ownership x≠tid)) (tee_memories (TEE_state s')))
              ⟶ {x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
                           {x. x∈set((tee_memories (TEE_state s')))∧ (ownership x≠tid)})"
  apply auto
  using  member_filter 
  apply (metis (mono_tags) filter_set) 
  by (metis (mono_tags) filter_set member_filter)


subsection "API related"        

lemma OpenSessionEntryPoint_not_change_REE:"∀s sc opt tid. REE_state (TA_OpenSessionEntryPoint sc s opt tid) = REE_state s" 
using TA_OpenSessionEntryPoint_def apply simp 
apply(rule someI)
using some_eq_imp 
by (metis (mono_tags, lifting))


lemma OpenSessionEntryPoint_about_other_TA:"∀s sc opt tid. ( filter (λx. ownership x≠tid) (tee_memories(TEE_state (TA_OpenSessionEntryPoint sc s opt tid)) )  
                                                  =( filter (λx. ownership x≠tid) (tee_memories(TEE_state s))))" 
using TA_OpenSessionEntryPoint_def apply simp 
apply(rule someI) 
using some_eq_imp 
by (metis (mono_tags, lifting))

lemma OpenSessionEntryPoint_about_TEE:"∀s sc opt tid. ( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state (TA_OpenSessionEntryPoint sc s opt tid)) )  
                                                  =( filter (λx. block_id x=(0::nat)) (tee_memories(TEE_state s))))" 
using TA_OpenSessionEntryPoint_def apply simp 
apply(rule someI) 
using some_eq_imp 
by (metis (mono_tags, lifting))

(* by (metis (mono_tags, lifting) verit_sko_ex') *)

lemma OpenSessionEntryPoint_not_change_TEE_aux:"({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
                           {x. x∈set(tee_memories (TEE_state (TA_OpenSessionEntryPoint sc s opt tid)))∧ (block_id x=0)})" 
  using OpenSessionEntryPoint_about_TEE filter_related by blast

lemma OpenSessionEntryPoint_not_change_TEE:"∀s sc opt tid. ({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
                           {x. x∈set(tee_memories (TEE_state (TA_OpenSessionEntryPoint sc s opt tid)))∧ (block_id x=0)})" 
    using OpenSessionEntryPoint_not_change_TEE_aux by blast


lemma OpenSessionEntryPoint_not_change_other_TA_aux:"{x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
                           {x. x∈set((tee_memories (TEE_state (TA_OpenSessionEntryPoint sc s opt tid))))∧ (ownership x≠tid)}"
    using OpenSessionEntryPoint_about_other_TA filter_related_TA by blast

lemma OpenSessionEntryPoint_not_change_other_TA:"∀s sc opt tid. {x. x∈set((tee_memories (TEE_state s)))∧ (ownership x≠tid)} =
                           {x. x∈set((tee_memories (TEE_state (TA_OpenSessionEntryPoint sc s opt tid))))∧ (ownership x≠tid)}"
    using OpenSessionEntryPoint_not_change_other_TA_aux  by blast


lemma OpenSessionEntryPoint_not_change_mem:"∀s sc opt tid. ((tee_memories (TEE_state (s))) =
                            tee_memories(TEE_state (TA_OpenSessionEntryPoint sc s opt tid)))"
                            by (metis (mono_tags, lifting) TA_OpenSessionEntryPoint_def someI2)
    



lemma TA_Memory_Init_not_change_TEE_aux:"({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
                           {x. x∈set(tee_memories (TEE_state (fst(TA_Memory_Init s sc size1 tid))))∧ (block_id x=0)})" 
proof -
{
  define s' where "s' = (fst(TA_Memory_Init s sc size1 tid))"
  let ?s1 = "(let
                                          
                                            new_total = (tee_total_size (TEE_state s)) -size1;
                                            new_memList = ⦇block_id = newMemBlockID3 s,size=size1,ownership = tid,
                                              access_right =(λx. None)(tid:=Some READWRITE) ,is_SecureMem=True,related= None⦈#(tee_memories(TEE_state s));
                                         
                                              s1 = s⦇TEE_state:=(TEE_state s)
                                                  ⦇tee_total_size := new_total, tee_memories := new_memList,
                                                  ta_mgr:=ta_mgr(TEE_state s)⦇BIDpointer:=BIDpointer(ta_mgr (TEE_state s))+1 ⦈⦈⦈ in s1)"
  
    have a1:"s'=(let 
                                              
                                                  new_total1 = (tee_total_size (TEE_state ?s1)) -size1;
                                                new_memList1 = ⦇block_id = newMemBlockID3 ?s1,size=size1,ownership = tid,
                                              access_right = (λx. None)((TEE sc):=Some READ) ,is_SecureMem=True,related =None⦈#(tee_memories(TEE_state ?s1));
                                              
                                              s2 =?s1⦇TEE_state:=(TEE_state ?s1)
                                                  ⦇tee_total_size := new_total1, tee_memories := new_memList1,
                                                   ta_mgr:=ta_mgr(TEE_state ?s1)⦇BIDpointer:=BIDpointer(ta_mgr (TEE_state ?s1))+1 ⦈⦈⦈ in 
                                                s2)" using TA_Memory_Init_def  by (metis fst_conv s'_def)
  have a2:"(filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state s))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state ?s1)))"
      using  newMemBlockID3_def by auto
  have a3:"(filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state ?s1))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state s')))"
            using newMemBlockID3_def a1 by simp
  have a4:"(filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state s))) = (filter (λx. (block_id x) = (0::nat)) (tee_memories(TEE_state s')))"
            using a2 a3 by argo
  have a5:" filter (λx. block_id x = 0) (tee_memories (TEE_state s)) 
              = filter (λx. block_id x = 0) (tee_memories (TEE_state (fst (TA_Memory_Init s sc size1 tid))))" 
                using a4 s'_def by blast 
  show ?thesis using filter_related a5 by blast
}qed

lemma TA_Memory_Init_not_change_TEE:"∀s sc tid size1. ({x. x∈set(tee_memories (TEE_state (s)))∧ (block_id x=0)} =
                           {x. x∈set(tee_memories (TEE_state (fst(TA_Memory_Init s sc size1 tid))))∧ (block_id x=0)})"
                       using TA_Memory_Init_not_change_TEE_aux by blast

lemma TA_Memory_Init_not_change_otherTA_aux:"({x. x∈set(tee_memories (TEE_state (s)))∧ (ownership x≠tid)} =
                           {x. x∈set(tee_memories (TEE_state (fst(TA_Memory_Init s sc size1 tid))))∧ (ownership x≠tid)})" 
proof -
{
  define s' where "s' = (fst(TA_Memory_Init s sc size1 tid))"
  let ?s1 = "(let
                                          
                                            new_total = (tee_total_size (TEE_state s)) -size1;
                                            new_memList = ⦇block_id = newMemBlockID3 s,size=size1,ownership = tid,
                                              access_right =(λx. None)(tid:=Some READWRITE) ,is_SecureMem=True,related= None⦈#(tee_memories(TEE_state s));
                                         
                                              s1 = s⦇TEE_state:=(TEE_state s)
                                                  ⦇tee_total_size := new_total, tee_memories := new_memList,
                                                  ta_mgr:=ta_mgr(TEE_state s)⦇BIDpointer:=BIDpointer(ta_mgr (TEE_state s))+1 ⦈⦈⦈ in s1)"
  
    have a1:"s'=(let 
                                              
                                                  new_total1 = (tee_total_size (TEE_state ?s1)) -size1;
                                                new_memList1 = ⦇block_id = newMemBlockID3 ?s1,size=size1,ownership = tid,
                                              access_right = (λx. None)((TEE sc):=Some READ) ,is_SecureMem=True,related =None⦈#(tee_memories(TEE_state ?s1));
                                              
                                              s2 =?s1⦇TEE_state:=(TEE_state ?s1)
                                                  ⦇tee_total_size := new_total1, tee_memories := new_memList1,
                                                   ta_mgr:=ta_mgr(TEE_state ?s1)⦇BIDpointer:=BIDpointer(ta_mgr (TEE_state ?s1))+1 ⦈⦈⦈ in 
                                                s2)" using TA_Memory_Init_def  by (metis fst_conv s'_def)
  have a2:"(filter (λx. (ownership x≠tid)) (tee_memories(TEE_state s))) = (filter (λx. (ownership x≠tid)) (tee_memories(TEE_state ?s1)))"
            using newBlockID_not_zero filter_pre by auto
  have a3:"(filter (λx. (ownership x≠tid)) (tee_memories(TEE_state ?s1))) = (filter (λx. (ownership x≠tid)) (tee_memories(TEE_state s')))"
            using newBlockID_not_zero filter_pre a1 by simp
  have a4:"(filter (λx. (ownership x≠tid)) (tee_memories(TEE_state s))) = (filter (λx. (ownership x≠tid)) (tee_memories(TEE_state s')))"
            using a2 a3 by argo
  have a5:" filter (λx. (ownership x≠tid)) (tee_memories (TEE_state s)) 
              = filter (λx. (ownership x≠tid)) (tee_memories (TEE_state (fst (TA_Memory_Init s sc size1 tid))))" 
                using a4 s'_def by blast 
  show ?thesis using filter_related_TA a5 by blast
}qed

lemma TA_Memory_Init_not_change_otherTA:"∀s sc tid size1. ({x. x∈set(tee_memories (TEE_state (s)))∧ (ownership x≠tid)} =
                           {x. x∈set(tee_memories (TEE_state (fst(TA_Memory_Init s sc size1 tid))))∧ (ownership x≠tid)})"
                       using TA_Memory_Init_not_change_otherTA_aux by blast



lemma a222:"∀s tid1. system_time s =system_time (s⦇TEE_state:=(aa::TEE_TYPE)⦈)" 
by simp

lemma a223:"∀s tid1. REE_state s =REE_state (s⦇TEE_state:=(aa::TEE_TYPE)⦈)" 
by simp

lemma a224:"∀s. ree_total_size(REE_state s) =ree_total_size(REE_state (s⦇REE_state:=(REE_state s)⦇tee_ctx_list := x::TEE_CONTEXT_TYPE list⦈⦈)) ∧
   driver_mem(REE_state s) =driver_mem(REE_state (s⦇REE_state:=(REE_state s)⦇tee_ctx_list := x::TEE_CONTEXT_TYPE list⦈⦈))"  by simp

lemma a225:"∀s. tee_memories(TEE_state s) =tee_memories(TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr := x::TEE_TA_MANAGER⦈⦈))" by simp

lemma a226:"∀s. (TEE_state s) =(TEE_state (s⦇REE_state:=x::REE_TYPE⦈))" by simp


lemma MgrPostOperation_not_change_REE:"∀s  tid. REE_state (MgrPostOperation s tid) = REE_state s" 
              using MgrPostOperation_def a223 unsetBusyInstance_def by metis

lemma MgrPostOperation_not_change_TEE_mem:"∀s tid. tee_memories(TEE_state (MgrPostOperation s tid)) = tee_memories(TEE_state s)" 
              using MgrPostOperation_def a225 unsetBusyInstance_def by metis

lemma addREESession_not_change_REE_mem:"∀s ses_id ctx1. ree_total_size(REE_state(addREESession s ses_id ctx1)) =ree_total_size (REE_state s)∧
                                          driver_mem(REE_state(addREESession s ses_id ctx1)) =driver_mem (REE_state s)" 
using a224 addREESession_def by metis

lemma addREESession_not_change_TEE:"∀s ses_id ctx1. TEE_state(addREESession s ses_id ctx1) =(TEE_state s)" 
              using a226 addREESession_def by metis



lemma a111:"tee_memories(TEE_state s) = tee_memories(TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(x::TEE_TA_MANAGER)⦈⦈))" by simp

lemma a112:"ta_mgr(TEE_state s) = ta_mgr(TEE_state (s⦇TEE_state:=(TEE_state s)⦇tee_memories:=(x::MemBlock list),tee_total_size:=y::nat⦈⦈))" by simp

lemma a113:"tee_memories(TEE_state s) = tee_memories(TEE_state (s⦇current:=x::nat, exec_prime:=y::(EVENT_PARAM × EVENT_NAME) list⦈))" by simp

lemma a114:"REE_state s = REE_state (s⦇current:=z::nat,exec_prime:=x::(EVENT_PARAM × EVENT_NAME) list,TEE_state:=y::TEE_TYPE⦈)" by simp

lemma a1131:"tee_memories(TEE_state s) = tee_memories(TEE_state (s⦇exec_prime:=y::(EVENT_PARAM × EVENT_NAME) list⦈))" by simp

lemma a1141:"REE_state s = REE_state (s⦇exec_prime:=x::(EVENT_PARAM × EVENT_NAME) list,TEE_state:=y::TEE_TYPE⦈)" by simp


lemma a115:"tee_memories(TEE_state s) = tee_memories(TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(x::TEE_TA_MANAGER)⦈,TAs_state:=z::TAs_State⦈))" by simp

lemma a116:"BIDpointer(ta_mgr(TEE_state s)) = BIDpointer(ta_mgr(TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(ta_mgr (TEE_state s))⦇mgr_ta_instances:=(x::TA_INSTANCE_CTX_TYPE list)⦈⦈,TAs_state:=z::TAs_State⦈)))"
by simp

lemma a1161:"BIDpointer(ta_mgr(TEE_state s)) = BIDpointer(ta_mgr(TEE_state (s⦇TEE_state:=(TEE_state s)⦇ta_mgr:=(ta_mgr (TEE_state s))⦇mgr_ta_sessions:=q::TA_MGR_SESSION_TYPE list⦈⦈⦈)))"
by simp

lemma addMgrSession_not_change_REE:"∀s  ses_id. REE_state s =REE_state ( (addMgrSession s  ses_id)) "
        using addMgrSession_def a114
        by simp

lemma addMgrSession_not_change_BID:"∀s ses_id. BIDpointer(ta_mgr(TEE_state s)) = BIDpointer(ta_mgr(TEE_state  (addMgrSession s  ses_id))) "
    using addMgrSession_def a114
        by simp


lemma addMgrInstance_not_change_TEE_mem:"∀sc s id1 ses_id. tee_memories(TEE_state s) =tee_memories(TEE_state (fst (addMgrInstance s sc id1 ses_id))) "
        using addMgrInstance_def a115
        by (metis eq_fst_iff) 

lemma addMgrInstance_not_change_BID:"∀sc s id1 ses_id. BIDpointer(ta_mgr(TEE_state s)) = BIDpointer(ta_mgr(TEE_state (fst (addMgrInstance s sc id1 ses_id)))) "
        using addMgrInstance_def a116
        by (metis eq_fst_iff) 

lemma addMgrInstance_not_change_REE:"∀sc s id1 ses_id. tee_memories(TEE_state s) =tee_memories(TEE_state (fst (addMgrInstance s sc id1 ses_id))) "
        using addMgrInstance_def a115 
        by (metis fst_conv)


lemma addSesToInstance_not_change_TEE_mem:"∀s id1 ses_id. tee_memories(TEE_state s) =tee_memories(TEE_state (addSesToInstance s id1 ses_id)) "
        using addSesToInstance_def a111
        by metis 
       

lemma addSesToInstance_not_change_REE:"∀s id1 ses_id. REE_state s =REE_state (addSesToInstance s id1 ses_id) "
        using addSesToInstance_def 
        by (smt (verit, ccfv_SIG) State.cases State.select_convs(3) State.update_convs(4)) 
        
       


        

lemma InitMgrSession_not_change_TEE_mem:"∀sc s tid1 ses_id cli. tee_memories(TEE_state s) =tee_memories(TEE_state ( (InitMgrSession s cli ses_id  tid1))) "
        using InitMgrSession_def a111 
        by metis

lemma InitMgrSession_not_change_REE:"∀sc s tid1 ses_id cli. REE_state s =REE_state ( (InitMgrSession s cli ses_id tid1)) "
        using InitMgrSession_def 
        by (metis (no_types, lifting) State.select_convs(3) State.surjective State.update_convs(4)) 
      
       
lemma plusRefInstance_not_change_TEE_mem:"∀s uuid. tee_memories(TEE_state s) =tee_memories(TEE_state ( (plusRefInstance s uuid))) "
        using plusRefInstance_def a111 
        by (metis)

lemma plusRefInstance_not_change_REE:"∀s uuid. REE_state s =REE_state ( (plusRefInstance s uuid)) "
        using plusRefInstance_def 
        by (metis (no_types, lifting) State.select_convs(3) State.surjective State.update_convs(4)) 
      

lemma setBusyInstance_not_change_TEE_mem:"∀s uuid. tee_memories(TEE_state s) =tee_memories(TEE_state ( (setBusyInstance s uuid))) "
        using setBusyInstance_def a111 
        by (metis)

lemma setBusyInstance_not_change_REE:"∀s uuid. REE_state s =REE_state ( (setBusyInstance s uuid)) "
        using setBusyInstance_def 
       by (metis (no_types, lifting) State.select_convs(3) State.surjective State.update_convs(4))

(*
lemma TA_Memory_Init_not_change_mgr:"∀sc s tid size1. ta_mgr(TEE_state s) = ta_mgr(TEE_state (fst(TA_Memory_Init s sc size1 tid)))" 
              using a112 TA_Memory_Init_def newMemBlockID3_def by auto
*)

lemma TA_Memory_Init_not_change_REE:"∀sc s tid size1. (REE_state s) = REE_state (fst(TA_Memory_Init s sc size1 tid))" 
              using a112 TA_Memory_Init_def newMemBlockID3_def by auto



end